--------------------------------------------------------------------------------
--
--  Murphi Model of the HyperWall Architecture
--
--------------------------------------------------------------------------------
--
--  version:      1.0
--
--  written by:   Jason Bau
--  date:         November 2011
--  affiliation:  Stanford University (research assistant)
--
--------------------------------------------------------------------------------
--
--  Modeling the Trust Evidence Telemetry Protocol
--
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- constants, types and variables
--------------------------------------------------------------------------------


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const
  --first we have the model options.
  SENDIPHIMH: false;     --Are IPH and IMH sent in the protocol?
  CHECKSIGS:  true;     --Should we check signatures? (Should fail if we don't)
  CHECKNONCE: true;     --Should we check nonces? (Should fail if we don't)

  NumCustomers:    2;   -- number of Customers
  NumHyperVisors:  2;   -- number of HyperVisors (these are the attackers)
  NumCPUs:         2;   -- number of CPUs
  VMsPerCust:      1;   -- number of VMs each Customer owns
  QueriesPerVM:    3;   -- number of times each customer tries to query each VM
  NumVMs:          NumCustomers*VMsPerCust;   -- max number of total VMs
  MaxNonce:        2*NumVMs*QueriesPerVM;  -- max number of nonces
  MaxPSVal:        MaxNonce;
  MaxIMIP:         NumVMs*NumVMs;
  NetworkSize:     10;  -- number of requests and responses for VM creation  
  HVMemory:        10;   -- number of each signature HV remembers
-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
type
  CustomerId:    scalarset (NumCustomers);   -- identifiers
  HyperVisorId:  scalarset (NumHyperVisors);
  VMId:          scalarset (NumVMs);
  CPUId:         scalarset (NumCPUs);
  PrincipId:     union {CustomerId, HyperVisorId, CPUId};
  
  CurVM: 1..VMsPerCust;
  Nonce: 1..MaxNonce;
  PSVal: 1..MaxPSVal;
  CurQuery: 1..QueriesPerVM;
  IMIP:  0..MaxIMIP; -- a serial number for the IM and IP (enumerated together)

  CPUType : enum {
	C_HyperWall,
	C_NoHyperWall
  };

  CPU : record
    HV: HyperVisorId;            -- Which Hypervisor is running on me?
    cType: CPUType;
  end;

  VM : record 
    CPU: CPUId;                  -- what CPU did this VM start on
    NC: Nonce;                   -- Nonce of last customer request
    IP: IMIP;                    -- Initial protection  
    IM: IMIP;                    -- Initial memory (IP and IM make up SSData)
  end;


  PS : record                    -- the values preserved in the signed hash.  Attackers can''t write this structure w/o key
    signedBy: PrincipId;         -- what principal signed this  
    NC: Nonce;                   -- Nonce of last customer request
    VID: VMId;                   -- which VM Sig refers to
    IP: IMIP;                    -- Initial protection 
    IM: IMIP;                    -- Initial memory 
    PSData: PSVal;               -- Who wrote the PSData (CPU or Attacking HV)
  end;


  MessageType : enum {           -- different types of messages
	M_VMRequest,                 -- request for VM creation
	M_VMResponse                 -- response (ack) for VM creation
  };

  Message : record
    source:   PrincipId;         -- source of message
    dest:     PrincipId;         -- intended destination of message
    mType:    MessageType;       -- type of message
    NC:       Nonce;             -- nonce (NC)
    VID:      VMId;              -- VM Id
    PS:       PS;                -- Signature over PSData
    PSData:   PSVal;             -- Who wrote the PSData (CPU or Attacking HV)
    WhoWrotePSData: PrincipId;   -- Is PSData legit or forged (this value is by the verification to track)
  end;


  CustomerStates : enum {
    C_SLEEP,                     -- state after initialization, will request VM creation
    C_WAITFORHV,                 -- customer waiting for msg from HV
    C_COMMIT                     -- customer commits to created VM
  };                             

   
  CustVM : record  -- Data structure kept by customer for each of her VMs
    VID: VMId;             -- VID
    curQuery: CurQuery;    -- which query are we on?
    resultFrom: PrincipId; -- where did we get the last accepted result from?
    NC: Nonce;	           -- Nonce for this query
    CPU: CPUId;            -- Which CPU do we expect
    HV: HyperVisorId;      -- Which HyperVisor controls this VM
    IM: IMIP;              -- Initial Image
    IP: IMIP;              -- Initial IP
  end;

  Customer : record
    state: CustomerStates;
    curVM: CurVM;
    VMs: array[CurVM] of CustVM
  end;                          

  HyperVisorStates : enum {
    H_SLEEP,
    H_DONE
  };

  HyperVisor : record
    state:  HyperVisorStates;
    resps: multiset[HVMemory] of Message; 
  end;

  GlobalStates : enum {
    INIT1,
    INIT2,
    RUN
  };
 
  
    

-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
var                                         -- state variables for
  cust: array[CustomerId] of Customer;      --  Customers
  hype: array[HyperVisorId] of HyperVisor;  --  HyperVisors 
  net:  multiset[NetworkSize] of Message;
  cpu:  array[CPUId] of CPU; 
  vms:  array[VMId] of VM;
  nextNonce:    Nonce;
  nextIMIP:     IMIP;
  nextPSVal:    PSVal;
  globalState:  GlobalStates;


---functions-------------

-- Generate a fresh nonce

function freshNonce(): Nonce;
var tmp: Nonce;
begin
  if nextNonce = MaxNonce then
     error "Ran out of nonces!"
  end;
  tmp := nextNonce;
  nextNonce := nextNonce + 1;
  return tmp;
end;

-- Generate a next IMIP nonce

function getIMIP(): IMIP;
var tmp: IMIP;
begin
  if nextIMIP = MaxIMIP then
     error "Ran out of IMIPs!"
  end;
  tmp := nextIMIP;
  nextIMIP := nextIMIP + 1;
  return tmp;
end;

-- Generate a PSVal

function getPSVal(): PSVal;
var tmp: PSVal;
begin
  if nextPSVal = MaxPSVal then
     error "Ran out of PSVals!"
  end;
  tmp := nextPSVal;
  nextPSVal := nextPSVal + 1;
  return tmp;
end;


--------------------------------------------------------------------------------
-- rules
--------------------------------------------------------------------------------


--------------------------------------------------------------------------------
-- behavior of Customers

-- customer i requests VM with HyperVisor j 
ruleset i: CustomerId do
    rule 20 "customer queries HV for VM protections"
      globalState = RUN &
      cust[i].state = C_SLEEP &
      cust[i].curVM <= VMsPerCust &
      cust[i].VMs[cust[i].curVM].curQuery <= QueriesPerVM &
      multisetcount (l:net, true) < NetworkSize

    ==>
    
    var
      outM: Message;   -- outgoing message

    begin
      undefine outM;
      outM.source  := i;
      outM.dest    := cust[i].VMs[cust[i].curVM].HV;
      outM.mType   := M_VMRequest;
      outM.NC	   := freshNonce();
      outM.VID     := cust[i].VMs[cust[i].curVM].VID;

      multisetadd (outM,net);

      cust[i].VMs[cust[i].curVM].NC       :=outM.NC;
      cust[i].state                       :=C_WAITFORHV;
    end;
end;

-- customer i reacts to message received
ruleset i: CustomerId do
  choose j: net do
    rule 20 "customer reacts to message received from HV"
      globalState = RUN &
      cust[i].state = C_WAITFORHV &
      net[j].dest = i 
    ==>

    var
      inM:  Message;   -- incoming message

    begin
      inM := net[j];
      multisetremove (j,net);

      if inM.mType=M_VMResponse then   -- correct message type
            --customer validation of signatures
          if (
		  (!CHECKSIGS  | inM.PS.signedBy=cust[i].VMs[cust[i].curVM].CPU) &  --check signature 
		  (!CHECKNONCE | inM.PS.NC=cust[i].VMs[cust[i].curVM].NC) &         --check freshness by right nonce
	          (inM.PS.VID = cust[i].VMs[cust[i].curVM].VID) &                   --check we got the right VID
		  (inM.PS.PSData = inM.PSData)                                      --checking PS
		  )
          then 
            cust[i].VMs[cust[i].curVM].resultFrom := inM.WhoWrotePSData; -- record result
          else
            --error "initiator received incorrect nonce"
          end; 
	  -- set the next VM query
          if (cust[i].VMs[cust[i].curVM].curQuery < QueriesPerVM) then
	     cust[i].state := C_SLEEP;
             cust[i].VMs[cust[i].curVM].curQuery := cust[i].VMs[cust[i].curVM].curQuery + 1;
          else 
             if (cust[i].curVM < VMsPerCust) then
                cust[i].state := C_SLEEP;
                cust[i].curVM := cust[i].curVM + 1;
                cust[i].VMs[cust[i].curVM].curQuery := 1;
             else
	        cust[i].state := C_COMMIT;
                --error "finished all queries"
             end;
          end;
       end;
     end;
  end;
end;


--------------------------------------------------------------------------------
-- behavior of HyperVisors
-- appropriate behavior first
-- HyperVisor i reacts to Customer''s request
ruleset i: HyperVisorId do
  choose j: net do
    rule 20 "Hypervisor receives telemetry request, behaves honestly (but records signatures and response)"
      globalState = RUN &
      hype[i].state = H_SLEEP &
      net[j].dest = i 

    ==>

    var
      outM: Message;   -- outgoing message
      inM:  Message;   -- incoming message

    begin
          inM := net[j];
          multisetremove (j,net);



        
          --CPU signs and sends out reply, which the HV does not change
                        undefine outM;
  			outM.source  := i;
			outM.dest    := inM.source;   
			outM.mType   := M_VMResponse;

                      
			outM.PS.signedBy:=vms[inM.VID].CPU;
                        outM.PS.NC:=inM.NC;
			outM.PS.VID:=inM.VID;
			outM.PS.PSData:=getPSVal();
			outM.PSData:=outM.PS.PSData;
			outM.WhoWrotePSData:=vms[inM.VID].CPU;
		        
			if (SENDIPHIMH) then
			  outM.PS.IP := vms[inM.VID].IP;
			  outM.PS.IM := vms[inM.VID].IM;
                        end;

          --Record signatures and response
                        multisetadd (outM,hype[i].resps);

	  --Send response
                        multisetadd (outM,net);

          --hype[i].state     := H_DONE;
		  
    end;
  end; 
end;

-- HyperVisor i reacts to Customer''s request
ruleset i: HyperVisorId do
  choose j: net do
    rule 20 "Hypervisor receives telemetry request, makes up and signs its own value"
      globalState = RUN &
      hype[i].state = H_SLEEP &
      net[j].dest = i 

    ==>

    var
      outM: Message;   -- outgoing message
      inM:  Message;   -- incoming message

    begin
          inM := net[j];
          multisetremove (j,net);
        
          --HV Makes up a value
                        undefine outM;
  			outM.source  := i;
			outM.dest    := inM.source;   
			outM.mType   := M_VMResponse;

                      
			outM.PS.signedBy:=i; --HV has to sign
                        outM.PS.NC:=inM.NC;
			outM.PS.VID:=inM.VID;
			outM.PS.PSData:=getPSVal();
			outM.PSData:=outM.PS.PSData;
			outM.WhoWrotePSData:=i;
		        
			if (SENDIPHIMH) then
			  outM.PS.IP := vms[inM.VID].IP;
			  outM.PS.IM := vms[inM.VID].IM;
                        end;


	  --Send response
                        multisetadd (outM,net);

          --hype[i].state     := H_DONE;
		  
    end;
  end; 
end;

ruleset i: HyperVisorId do
  choose k: hype[i].resps do
  choose j: net do
    rule 20 "Hypervisor receives telemetry request, replays a recorded value"
      globalState = RUN &
      hype[i].state = H_SLEEP &
      net[j].dest = i 

    ==>

    var
      outM: Message;   -- outgoing message
      inM:  Message;   -- incoming message

    begin
          inM := net[j];
          multisetremove (j,net);
        
          --HV Makes up a value
                        undefine outM;
  			outM.source  := i;
			outM.dest    := inM.source;   
			outM.mType   := M_VMResponse;

                      
			outM.PS.signedBy:=hype[i].resps[k].PS.signedBy; 
                        outM.PS.NC:=hype[i].resps[k].PS.NC;
			outM.PS.VID:=hype[i].resps[k].PS.VID;
			outM.PS.PSData:=hype[i].resps[k].PS.PSData;
			outM.PSData:=hype[i].resps[k].PSData;
			outM.WhoWrotePSData:=i;
		        
			if (SENDIPHIMH) then
			  outM.PS.IP := hype[i].resps[k].PS.IP;
			  outM.PS.IM := hype[i].resps[k].PS.IM;
                        end;


	  --Send response
                        multisetadd (outM,net);

          --hype[i].state     := H_DONE;
		  
    end;
  end; 
  end;
end;

--------------------------------------------------------------------------------
-- startstate
--------------------------------------------------------------------------------

startstate
  globalState := INIT1;
  nextNonce := 1;
  nextIMIP := 1;
  nextPSVal := 1;
  undefine vms;

  -- initialize initiators
  undefine cust;
  for i: CustomerId do
    cust[i].state     := C_SLEEP;
    cust[i].curVM := 1;
    for j:CurVM do 
      undefine cust[i].VMs[j];
      cust[i].VMs[j].curQuery := 1;
    end;
  end;

  -- initialize HyperVisors
  undefine hype;
  for i: HyperVisorId do
    hype[i].state     := H_SLEEP;
  end;

  -- initialze CPUs
  undefine cpu; 
  for i: CPUId do 
    cpu[i].cType  := C_HyperWall;
  end;
 
  -- initialize everything else
  undefine net;

end;

--- 
-- Some further initialization.  
---

-- Assign each CPU to a Hypervisor

ruleset c: CPUId do
 ruleset h: HyperVisorId do
   rule 50 "Assign CPU to Hypervisor"
      globalState = INIT1
   ==>
      cpu[c].HV:=h;
      if (forall p:CPUId do !isundefined(cpu[p].HV) endforall) then
         globalState := INIT2;
      end;
   end;
 end;
end;

-- Assign each VM to a CPU
ruleset k: CustomerId do
 ruleset j: CurVM do
 ruleset c: CPUId do
 ruleset i: VMId do
   rule 50 "Assign VMs to CPU"
      globalState = INIT2 &
      isundefined(vms[i].CPU) &
      isundefined(cust[k].VMs[j].CPU)
   ==>
      cust[k].VMs[j].VID := i;
      cust[k].VMs[j].CPU := c;
      cust[k].VMs[j].HV := cpu[c].HV;
      cust[k].VMs[j].IM := getIMIP();
      cust[k].VMs[j].IP := cust[k].VMs[j].IM;
      vms[i].CPU := c;
      vms[i].IP := cust[k].VMs[j].IP;
      vms[i].IM := cust[k].VMs[j].IM;
      if (forall cu:CustomerId do
           forall vm:CurVM do 
            !isundefined(cust[cu].VMs[vm].CPU) 
           endforall
         endforall) 
      then
         globalState := RUN;
	 --error "assigned VMs to CPUs"	
      end;
   end;
 end;
 end;
 end;
end;


invariant "Customer never accepts response tampered by HV"
forall c:CustomerId do
 forall v:CurVM do 
    !isundefined(cust[c].VMs[v].resultFrom) 
      ->
    !ismember(cust[c].VMs[v].resultFrom,HyperVisorId)
 end
end;
